package typesys;

import java.util.HashMap;
import java.util.HashSet;

import flowlogic.STSimplifier;

import ast.ChannelConstant;
import ast.Label;
import ast.Network;
import ast.NewConstN;
import ast.ParallelNetwork;
import ast.Procedure;
import ast.ProcessAtSite;
import ast.Site;
import ast.Term;

public class NetworkJudgement extends TypeJudgement {
	
	private Network network;
	private HashMap<String, HashSet<Term>> rho;
	private Label ctxLabel;
	private HashMap<String, Label> gamma;
	
	public NetworkJudgement(Network net, 
				Label ctxLabel, 
				HashMap<String, HashSet<Term>> rho,
				HashMap<String, Label> gamma,
				PrincipalHierarchy hierarchy) 
	{
		network = net;
		this.rho = rho;
		this.ctxLabel = ctxLabel;
		this.gamma = gamma;
		setHierarchy(hierarchy);
	}
	
	public boolean check() throws FunctionUndefinedException
	{
		boolean result = false;
		
		if (network instanceof ParallelNetwork) {
			
			result = true;
			for (Network net : ((ParallelNetwork) network).getComponentNetworks()) {
				NetworkJudgement netjdgt = new NetworkJudgement(
						net, ctxLabel, rho, gamma, getHierarchy());
				if (!netjdgt.check()) {
					result = false;
					break;
				}
			}
			
		} else if (network instanceof NewConstN) {
			
			HashMap<String, Label> gammaInner = null;
			if (((NewConstN) network).getConstant() instanceof ChannelConstant) {
				gammaInner = new HashMap<String, Label>();
				gammaInner.putAll(gamma);
				ChannelConstant cst = (ChannelConstant) ((NewConstN) network).getConstant();
				gammaInner.put(cst.getName(), cst.getLabel());
			} else {
				gammaInner = gamma;
			}
			
			NetworkJudgement netjdgt = new NetworkJudgement(
					((NewConstN) network).getNetwork(), 
					ctxLabel, rho, gammaInner, getHierarchy());
			result = netjdgt.check();
			
		} else if (network instanceof ProcessAtSite) {
			
			ProcessJudgement pjdgt = new ProcessJudgement(
					((ProcessAtSite) network).getProcess(),
					ctxLabel, rho, ((ProcessAtSite) network).getSite(), gamma, getHierarchy());
			
			result = pjdgt.check();
			
		}
		
		return result;
	}
}
